00100	
00200	CHOICE-STRATEGY-IS: 
00300	ANCESTRY∧SUPPORT[THM];
00400	
00500	EDIT-STRATEGY-IS: 
00600	DEPTH[1]∨LENGTH[5];
00700	
00800	ELAPSED-TIME =63351
00900	
01000	NIL 1 5
01100	1 S(THM2,THM3,THM3,THM1);3 4
01200	3 S(THM3,THM1,THM2,THM3);5 6
01300	4 S(z,u,x,y)⊃S(x,y,z,u);A2
01400	5 S(y,x,z,u)⊃S(x,y,z,u);A3
01500	6 S(THM1,THM3,THM2,THM3);THM